Decidability and Combination Results for Two Notions of Knowledge in Security Protocols
Identifieur interne : 003095 ( Main/Exploration ); précédent : 003094; suivant : 003096Decidability and Combination Results for Two Notions of Knowledge in Security Protocols
Auteurs : Véronique Cortier [France] ; Stéphanie Delaune [France]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2012-04-01.
English descriptors
- KwdEn :
- mix :
Abstract
Abstract: In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties $(\textsf{AC})$ . In this paper, we show that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. We also propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal) of equational theories involving $\textsf{AC}$ operators. As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.
Url:
DOI: 10.1007/s10817-010-9208-8
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000663
- to stream Istex, to step Curation: 000658
- to stream Istex, to step Checkpoint: 000857
- to stream Hal, to step Corpus: 001A84
- to stream Hal, to step Curation: 001A84
- to stream Hal, to step Checkpoint: 001965
- to stream Main, to step Merge: 003152
- to stream Main, to step Curation: 003095
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Decidability and Combination Results for Two Notions of Knowledge in Security Protocols</title>
<author><name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name>
</author>
<author><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:1D13B059946DF0F0A41581E5B28298A82B3E6735</idno>
<date when="2010" year="2010">2010</date>
<idno type="doi">10.1007/s10817-010-9208-8</idno>
<idno type="url">https://api.istex.fr/ark:/67375/VQC-2MJ8BTMR-R/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000663</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000663</idno>
<idno type="wicri:Area/Istex/Curation">000658</idno>
<idno type="wicri:Area/Istex/Checkpoint">000857</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000857</idno>
<idno type="wicri:doubleKey">0168-7433:2010:Cortier V:decidability:and:combination</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00525778</idno>
<idno type="url">https://hal.inria.fr/inria-00525778</idno>
<idno type="wicri:Area/Hal/Corpus">001A84</idno>
<idno type="wicri:Area/Hal/Curation">001A84</idno>
<idno type="wicri:Area/Hal/Checkpoint">001965</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">001965</idno>
<idno type="wicri:doubleKey">0168-7433:2012:Cortier V:decidability:and:combination</idno>
<idno type="wicri:Area/Main/Merge">003152</idno>
<idno type="wicri:Area/Main/Curation">003095</idno>
<idno type="wicri:Area/Main/Exploration">003095</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Decidability and Combination Results for Two Notions of Knowledge in Security Protocols</title>
<author><name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA, CNRS, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LSV, ENS de Cachan & CNRS & INRIA, 61 avenue du Président Wilson, 94235, Cachan Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Île-de-France</region>
<settlement type="city">Cachan</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Journal of Automated Reasoning</title>
<title level="j" type="abbrev">J Autom Reasoning</title>
<idno type="ISSN">0168-7433</idno>
<idno type="eISSN">1573-0670</idno>
<imprint><publisher>Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="2012-04-01">2012-04-01</date>
<biblScope unit="volume">48</biblScope>
<biblScope unit="issue">4</biblScope>
<biblScope unit="page" from="441">441</biblScope>
<biblScope unit="page" to="487">487</biblScope>
</imprint>
<idno type="ISSN">0168-7433</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0168-7433</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Equational theories</term>
<term>Formal methods</term>
<term>Security protocols</term>
</keywords>
<keywords scheme="mix" xml:lang="en"><term>Equational theories</term>
<term>Formal methods</term>
<term>Security protocols</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties $(\textsf{AC})$ . In this paper, we show that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. We also propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal) of equational theories involving $\textsf{AC}$ operators. As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
<li>Île-de-France</li>
</region>
<settlement><li>Cachan</li>
<li>Nancy</li>
</settlement>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name>
</region>
<name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name>
<name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name>
<name sortKey="Delaune, Stephanie" sort="Delaune, Stephanie" uniqKey="Delaune S" first="Stéphanie" last="Delaune">Stéphanie Delaune</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003095 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003095 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= ISTEX:1D13B059946DF0F0A41581E5B28298A82B3E6735 |texte= Decidability and Combination Results for Two Notions of Knowledge in Security Protocols }}
This area was generated with Dilib version V0.6.33. |